COM: rel 1 summary

COM: rel 1 intro

COM: binrel com

ABS: Refl(T;x,y.E(x;y))

STM: refl wf

STM: refl functionality wrt iff

ABS: Sym(T;x,y.E(x;y))

STM: sym wf

STM: sym functionality wrt iff

ABS: Trans(T;x,y.E(x;y))

STM: trans wf

STM: trans functionality wrt iff

STM: trans rel self functionality

ABS: EquivRel(T;x,y.E(x;y))

STM: equiv rel wf

STM: equiv rel subtyping

ABS: Preorder(T;x,y.R(x;y))

STM: preorder wf

COM: symmetrize com

ABS: Symmetrize(x,y.R(x;y);a;b)

STM: symmetrize wf

STM: symmetrized preorder

STM: trans rel func wrt sym self

STM: equiv rel iff

STM: equiv rel functionality wrt iff

COM: equiv rel self fun com

STM: equiv rel self functionality

STM: squash thru equiv rel

ABS: IsEqFun(T;eq)

STM: eqfun p wf

STM: sq stable eqfun p

ABS: AntiSym(T;x,y.R(x;y))

STM: anti sym wf

STM: anti sym functionality wrt iff

ABS: StAntiSym(T;x,y.R(x;y))

STM: st anti sym wf

ABS: strict_part(x,y.R(x;y);a;b)

STM: strict part wf

STM: strict part irrefl

ABS: Connex(T;x,y.R(x;y))

STM: connex wf

STM: connex functionality wrt iff

STM: connex functionality wrt implies

STM: connex iff trichot

ABS: Order(T;x,y.R(x;y))

STM: order wf

STM: order functionality wrt iff

ABS: Linorder(T;x,y.R(x;y))

STM: linorder wf

STM: linorder functionality wrt iff

STM: sq stable refl

STM: sq stable sym

STM: sq stable trans

STM: sq stable anti sym

STM: sq stable connex

STM: order split

ABS: Irrefl(T;x,y.E(x;y))

STM: irrefl wf

STM: trans imp sp trans

STM: trans imp sp trans a

STM: trans imp sp trans b

STM: linorder le neg

STM: linorder lt neg

COM: rel 1 end